1. Field of the Invention
The present invention relates generally to a computer implemented method, data processing system, and computer program product for evaluating a design under test (DUT). More specifically, the present invention relates to formally verifying the error bounds of numerical algorithms implemented in computer hardware and/or computer instructions.
2. Description of the Related Art
Manufacturers and developers of integrated circuits, commonly referred to as chips, rely on bits to provide binary representations of numbers. An acceptable drawback to this approach is that some rational non-integer numbers are approximated by rounding or otherwise dropping the least significant bits from a resultant calculation to provide an approximation of a numerical function. An approximation can be a truncation of one or more least significant bits, or other rounding that may adjust a result of a computation to a less than accurate final or intermediate result. The drawback is acceptable because the developers make promises concerning results of numeric functions, namely, that errors will remain within an accepted range or be bounded by an upper limit. Nevertheless, it can be a costly and time-consuming process to confirm such promises, also known as a specification. Normally, such a process confirms the algorithm before the algorithm is implemented in products. Nevertheless, the process influences product roll-out, acceptance of the product, and any later remedial work to compensate for a product that fails to meet the promises made earlier by the company.
Often, complex numerical functions, such as divide, square root, and trigonometric functions, are implemented as an iterative algorithm that approximates the infinitely precise result of a function. For example, a widely-known Newton-Raphson algorithm works as follows. It starts with an initial guess of a result for the implemented function, such as divide. Then, it applies mathematical operations to adjust the guess to more accurate approximations. After a number of iterations, a computer implementing the Newton-Raphson algorithm will result in an approximation that is very close to the infinitely precise result of the function. Finally, the last iteration is rounded to the finite precision result which will be returned by the algorithm.
In general, formal verification involves rigorously proving that a computing system satisfies an associated specification. In certain cases, the specification of a numerical computation can be given as a mathematical formula that sets an upper bound to errors tolerated in the computation for all inputs that the computation is expected to solve. In the case of divide, square root, and trigonometric functions, the correctness can be given as a mathematical formula that bounds the error of the approximation before the final rounding. A formal verification program checks that the specification is met by applying a number of programs such as bit-level equivalence checkers, model checkers, and theorem provers. It is important to recognize, that the implementing of such a function is frequently only approximated by the result given by the implemented formula that approximates the function. Thus, an approximation of a numerical function is the combined output produced or predicted to be produced by a data processing system that implements the approximated function with a series of finite precision outputs.
Numerical computation of computer hardware and software, for example floating-point systems, can be formally verified. Automated approaches, like bit-level equivalence checking, have been used to verify relatively simple floating point operations, such as add or multiply operations. However, the bit-level model checking fails to scale well to more complex mathematical operations, such as divide, square root, and trigonometric functions.
Other techniques such as mechanical theorem proving have been successfully used to verify such complex mathematical operations. However, mechanical theorem proving require tedious manual interactions between the computer and human experts. This cost makes mechanical theorem proving for numerical functions impractical in many cases. In the past, there is no known technique that can automatically verify complex numerical functions such as divide, square root, and trigonometric functions.